import org.jcsp.lang.*;

class Security implements CSProcess {

  protected AltingChannelInputInt down, up;
  protected ChannelOutputInt report;

  protected final int maxSitting;

  public Security (AltingChannelInputInt down, AltingChannelInputInt up,
                   ChannelOutputInt report, int maxSit) {
    this.down = down;
    this.up = up;
    this.report = report;
    this.maxSitting = maxSit;
  }

  public void run () {

    final Alternative alt = new Alternative (new Guard[] {down, up});
    boolean[] precondition = {true, true};
    final int DOWN = 0;
    final int UP = 1;

    int nSitting = 0;

    while (true) {
      report.write (nSitting);
      precondition[DOWN] = (nSitting < maxSitting);
      switch (alt.fairSelect (precondition)) {
        case DOWN:
          down.read ();
          nSitting++;
        break;
        case UP:
          up.read ();
          nSitting--;
        break;
      }
    }
  }

}
